Inference at * 2 2 1 2 1 1 
Iof proof for Lemma p-fun-exp-add-sq:



1. A : Type
2. f : A(A + Top)
3. x : A
4. m : 
5. 0 < m
6. n:. (can-apply(f^m - 1;x))  ((f^n+(m - 1)(x)) ~ (f^n(do-apply(f^m - 1;x))))
7. n : 
8. can-apply(f^m;x)
9. (n = 0)
10. (n+m = 0)
11. (n = 0)
12. (m = 0)
13. can-apply(f^m - 1;x)
14. x1 : A
15. do-apply(f^m - 1;x) = x1
  (f o f^n  (x1)) ~ (f o f^n - 1  (outl(f(x1)))) 

latex

 by (RepUR ``p-compose can-apply do-apply `` ( 0)) 
CollapseTHEN ((Subst' (f^n(x1))
CollapseTHEN ((Subst' (f^n(x1))~
CollapseTHEN ((Subst' (f^n(x1))(f^n - 1(outl(f(x1))))
Co( 0)) 
CollapseTHEN (((Try (Trivial))) 
CollapseTHEN ((Fold `do-apply` 0) 
CollapseTHEN ((
CRWO "p-fun-exp-add1-sq<" 0) 
CollapseTHENA (Auto))))) 

latex

C1: 

C1:   can-apply(f;x1)
C2: 

C2:   (f^n(x1)) ~ (f^(n - 1)+1(x1))
C.

Definitions	s ~ t, f^n, n - m, #$n, outl(x), f(a), f o g  , can-apply(f;x), do-apply(f;x), x:A. B(x), P  Q
Lemmas	p-fun-exp-add1-sq